COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.at "$¬"⊂"%f¬%1"⊃ <<reduces-stared>>
C00006 00003	.SS(Completeness Results)
C00017 00004	.end "on |]"
C00018 ENDMK
C⊗;
.at "$¬"⊂"%f¬%1"⊃ <<reduces-stared>>
.at "$→"⊂"%f→%1"⊃ <<reduces>>
.at "$e"⊂"%2Eval%1"⊃
.SS(Computation)
We now consider LCF as a programming language. We consider only closed terms, 
thus we have already given up on the idea of a total decision procedure
for determining provability (not unwise due to G⊗odel's results
and Theorem 19, section 4.4).

The %3programs%1 are closed terms of ground type. The idea is
that the ground terms are the data types and the programs produce data. 
The other terms are significant only as subterms of programs.

The operational semantics is given by a partial function,  $e,
which gives constants from programs. We define $e by means of an %3immediate
reduction relation%1,#$→, between terms by:

.begin center;

$e(?s) = ?c iff ?s $¬ ?c, for any program ?s and constant ?c.
.end

Where $¬ is the reflexive, transitive closure of $→. For this definition to make 
sense it is necessary that ?s#$¬#?c and ?s#$¬?c' implies
that ?c and ?c' are identical.
Notice that for constants, ?c, of ground type, $e(?c)#=#?c.

.group
The definition of $→ is given by the following reduction rules:


.begin tabit1(10);group
I\1. ∪(⊗T∪ → ∪s t)$→∪s∩
 \   ∪(⊗F∪ → ∪s t)$→∪t∩
 \   ∪(⊗U∪ → ∪s t)$→⊗U∩

\2. ∪Ys $→ ∪s(Ys)∩

\3. ∪((λx.s)t) $→ ∪[t/x]s∩
.apart
.group

II\1. ∪s $→ ∪s'∩
\ --------------
  \   ∪st $→ ∪s't∩

  \2. ∪s↓t $→ ∪s'↓t∩
\ --------------
  \   ∪(⊃s↓t∪) $→ ∪(⊃ s'↓t∪)∩

.end
.apart
 The operational semantics defined by $→ is part of the
provability relation, that is, if ?s#$→#?t then ?s#=?t is provable
in LCF (Lemma 8). The set of reduction rules have obvious counterparts
in the inference rules of the formal system. Notice that, because of I3 and II1,
function applications  are call by name rather than by value.

The behavior of a program, ?s, is determined by whether it terminates
and its value when it does; that is, whether $e(?s) exists
and which constant it is, if it does.

.SS(Completeness Results)
.begin "on |]"
.at "|"⊂"%f)%1"⊃
We say that a term ?s↓β is %3computable%1 iff it has the property
$C↓β defined by induction on types as follows:
.begin indent 10,10;
1.) If ?s↓β is a program, then ?s↓β has the property $C↓β iff
$A?s↓β|#=#$A?c| implies $e(?s)#=#?c.

2.) If ?s↓12 is a closed term, then it has property $C↓12 iff
whenever ?t↓1 is a closed term with property $C↓1, (?s↓12 ?t↓1)
has the property $C↓2.

3.) If ?s↓β is a term with free variables, ?x1n of
types β1,#...,#βn then it has the property $C↓β whenever
?N1n are closed terms having properties $C↓1,#...,#$C%4βn%1,
respectively.
.end

Clearly, if ?s↓12 and ?t↓1 are closed computable terms, so is ∪(st)∩.
Also a term ?s↓β where β#=#(β1#→#β2→,#...,#βn) is computable
iff ?s'?t%41%1#...#?t%4n-1%1 is computable whenever
?t%41%1,#...,#?t%4n-1%1 are closed computable terms  of the appropriate
types and ?s'↓β is a closed
instantiation of ?s↓β by computable terms. This can be proved by using clause 3)
of the definition if ?s↓β is open, and then clause 2) %3n%1 times.

The difficulty in proving all terms computable is caused by the fixed point 
operators, ∪Y↓3β. These can be approximated by the terms ∪Y%8n∩,#n≥0.

Letting ∪Y↓β be an abbreviation for ∪Y↓3β, note that
⊗U↓i#=#∪Y↓i∪(λx↓i∪.x↓i∪)∩ and ⊗U↓t#=#∪Y↓t∪(λx↓t∪.x↓t∪)∩⊗↓%1As an aid to
intuition: every element ?x is a fixed-point of the indentity function ∪λx.x∩, thus
the "least" fixed-point is the bottom element ⊗b. ⊗b↓β is the assignment
made to ⊗U↓β.← This can be proved by INDUCT, letting  πP be be the empty set
and πQ be ?x#=#⊗U.

Clearly, ⊗U↓12 = ∪λx↓1∪.⊗U↓2

.begin tabit1(20);group;

Define  ∪Y↓β%8n%1by:\∪Y↓β%80%1 = ⊗U↓3β, and
\∪Y↓β%8n+1%1 = ∪(λx.(x(Y↓β%8n∪x)))∩ with ∪x∩ of type β→β.
.end

?Y↓β%8n+1%1 is a function which for any argument ?x returns ∪x(Y↓β%8n∪x)∩ as
value. Leaving off the subscripts for easier reading, we have:
.begin tabit1(20);group;
\∪Y%80∪(x) = ∪UU(x) = UU∩ by MIN2
\∪Y%81∪(x) = x(Y%80∪x) = ∪x(UU)∩
\∪Y%82∪(x) = x(Y%81∪x) = ∪x(x(UU)) = x%82∪(UU)∩
\∪Y%83∪(x) = x(Y%82∪x) = ∪x(x%82∪(UU)) = x%83∪(UU)∩
\     ...	...	    ...
\∪Y%8n∪(x) = x(Y%8n-1∪x) = x%8n∪(UU)∩

.end
.turn off "{","}";
Then πl{$A?Y↓β%8n%1∪(x)∩|: n≥0} = πl{$A?x↓β%8n%1∪(UU)∩|: n≥0}. Suppose
that $A?x|#=#πf, then we have the above lubs
.begin tabit1(20);

\=#πl{πf%8n%1(⊗b): n≥0} = πY(πf),
.end
.turn on "{","}";
by the definition of the least fixed point operator, given back in Section 5.4,
{yon(R22)}.

.turn off "{","}";
Thus, since $A?Y↓β%8n∩(?x)| = $A?Y↓β%8n∩|($A?x|,
$A?Y↓β| = πl{$A?Y↓β%8n%1|: n≥0} expresses the LHS as the l.u.b. of a
denumerable chain for any standard interpretation ?A.
.turn on "{","}";

Remarks:
.begin indent 10,10;
1) Clearly ?Y↓β%8n%1 ≤?Y↓β for all β and n; and ⊗U↓β ≤ ?s↓β.

2) ?s↓β ≤ ?s↓β  by REFL

.R20:
3) If ?s↓12 ≤ ?s'↓12 and ?t↓1 ≤?t'↓1, then ∪(λx.s)∩ ≤ ∪(λx.s')∩
by ABSTR; and ∪(st)∩#≤#∪(s't')∩ since 
?s#≤#?s' implies  ∪(fs)∩#≤∪(fs')∩, by APPL; take ∪f#≡#λg.gt∩;
by CONV we have ∪(fs)#=#(st)∩ and ∪(fs')#=#(s't)∩; also by APPL:
∪(s't)∩#≤#∪(s't')∩; thus by TRANS  ∪(st)∩#≤#∪(s't')∩.
.end

%7LEMMA 6%1 If ?s ≤ ?t and ?s $→ ?s', then either ?s'#≤#?t or else for some ?t',
?t#$→#?t' and ?s'#≤#?t'.
.begin indent 10,10;
Proof is by structural induction and cases from which it is possible that ?s$→?s'.
See Plotkin[11].
.end

%7LEMMA 7%1 Every term is computable.

Proof:
.begin indent 10,10;
1. Every variable is computable since any closed instantiation of it by a 
computable term is computable.

2. Every constant other than the ?Y↓β's is computable.
For !t and !f this is clear. For ⊃↓t it is enough to show that ⊃↓β(⊗T#?s#?t)
is computable when ?s is a closed computable term; the other
cases being similar.
Suppose $A(⊗T→?s#?t)|#=#$A?c|. Then $A?s|#=#$A?c| since ?s is computable; this
implies $e(?s)#=#?c; i.e., ?s$¬?c; by the transitivity of $¬ we
have (⊗T→?s#?t)$¬?c; i.e. $e((⊗T→?s#?t))#=#?c.

3. If ?s↓12 and ?t↓1 are computable, so is ?s?t. If ?s?t is closed
then so are ?s and ?t and its computability follows from clause 2 of the definition of
$C. If ?s?t is open, any closed instantiation ?u of it by computable terms
has the form ?s'?t', where ?s' and ?t' are closed instantiations of
?s and ?t,
and are therefore computable, which again by clause 2 implies ?u is computable
and hence ?s?t is also.

4. If ?s↓2 is computable so is ∪(λx↓1∪.?s↓2∪)∩. It is enough to show that
the ground term ?u?t1N is computable when ?t1n are closed computable
terms and ?u is a closed instantiation of ∪(λx.s)∩ by computable terms.
?u must have the form ∪(λx.s')∩ where ?s' is an instantiation of all the
free variables of ?s, except ?x, by closed computable terms.
If $A?u?t1N|#=#$A?c|, then we have
$A[?t1/?x]?s'?t2N|#=#$A?u?t1N|#=#$A?c|. [?t1/?x]?s' is computable and thus so
is [?t1/?x]?s'?t2N. Therefore 
?u?t1N$→[?t1/?x]?s'?t2N$¬?c; i.e., $e(?u?t1N)#=#?c.

5. Each ?Y↓β is computable. It suffices to show that ?Y↓β?t1N is computable
when ?t1n are closed computable terms and ?Y↓β?t1N is ground.
Suppose $A?Y↓β?t1N|#=#$A?c|. Since $A?Y↓β|#=#πl%4k≥0$A?Y↓β%8k|,
$A?Y↓β%8k?t1N|#=#$A?c| for some %3k%1. $A⊗U↓β|#=#⊗b↓β for β ground; thus
 ⊗U↓β is computable for β ground.
From this and 1, 3, and 4, proved above it follows that every ⊗U↓β and
?Y↓β%8k%1 is computable. Thus ?Y↓β%8k?t1N$¬?c and so by lemma 6,
?Y↓β?t1N$¬?c.
.end
%7LEMMA 8%1 $e(?s) = ?c## =>## $ε?s = ?c. (i.e. $ε?s≤?c and $ε?c≤?s.)

Proof:
.begin indent 10,10;
1) If ?s is a constant, then ?s≡?c.

2) If ?s is not a constant, then there exists a sequence ?s = ?s1n = ?c,
such that each ?s%4i+1%1 follows from ?s%4i%1 by one of the rules
for $→.
We show that each rule of reduction can be derived from the axioms and
rules of inference; that is, we show ?s$→?t implies $ε?s#=#?t.
.begin TABIT2(15,40);
\I 1.a) $ε(⊗T→?s?t) = ?s\by CONDT
\    b) $ε(⊗F→?s?t) = ?t\by CONDF
\    c) $ε(⊗U→?s?t) = ⊗U\by CONDU
\  2. $ε?Y(?s) = ?s(?Y?s)\by FIXP
\  3. $ε∪((λx.s)t)∩ = ∪[t/x]s∩\by CONV

\II 1.if $ε?s = ?s' then $ε?s?t = ?s'?t\by 3) of Remarks, {yon(R20)}.
.end
.begin indent 15,15;
2. If $ε?s↓t = ?s'↓t then ?s and ?s' are syntactically identical since
⊗T and ⊗F are imcomparable and  ⊗T≤⊗U and  ⊗F≤⊗U. Thus $ε⊃?s↓t#=#⊃?s'↓t
by CONDT, CONDF, and CONDU.
.END
.END

%7THEOREM 9%1 For all programs ?s and constants ?c, the following
three statements are equivalent:
.begin tabit1(15);
\1. $ε?s = ?c is a theorem of LCF.
\2. $A?s| = $A?c|
\3. $e(?s) = ?c
.end
Proof:
.begin tabit1(15);
\1. => 2. by Theorem 5, section 6.2
\2. => 3. by Lemma 7
\3. => 1. by Lemma 8
.end

Thus in LCF, we have completeness among deduction,
truth, and computation for closed terms of ground type.
It is reasonable to consider only closed terms since, intuitively,
one could not expect a real  program to terminate if it had free variables
in it with no place to find their bindings.
.end "on |]"